package org.tau.workshop2011.semantics

import org.tau.workshop2011.expressions.Type
import org.tau.workshop2011.parsing.AST._
import java.lang.AssertionError

class NonLinearException extends Exception("The expression is not linear!")

case class LinearExpansion(var a: Int, var v: Variable, var b: Int) {
  if (v == null)
    assert(a == 0)

  if (a == 0) {
    v = null
  }

  def this(b: Int) = this(0, null, b)

  def this(a: Int, v: Variable) = this(a, v, 0)

  @throws(classOf[NonLinearException])
  def +(other: LinearExpansion): LinearExpansion = {
    if (!(this.v == other.v || this.v == null || other.v == null))
      throw new NonLinearException

    new LinearExpansion(
      this.a + other.a,
      if (this.v == null) other.v else this.v,
      this.b + other.b
    )
  }

  @throws(classOf[NonLinearException])
  def -(other: LinearExpansion): LinearExpansion = {
    this + other.copy (a = -other.a, b = - other.b)
  }

  @throws(classOf[NonLinearException])
  def *(other: LinearExpansion): LinearExpansion = {
    if (! (this.v == null || other.v == null))
      throw new NonLinearException

    val (num, lin) = if (this.v == null) (this, other) else (other, this)
    new LinearExpansion(
      lin.a * num.b,
      if (this.v == null) other.v else this.v,
      lin.b * num.b
    )
  }

  @throws(classOf[NonLinearException])
  def /(other: LinearExpansion): LinearExpansion = {
    if(! (other.v == null && other.b != 0))
      throw new NonLinearException

    new LinearExpansion(
      this.a / other.b,
      this.v,
      this.b / other.b
    )
  }

  def isConstant: Boolean = {
    a == 0
  }
}

/* Integer Expressions
 * ~~~~~~~~~~~~~~~~~~~
 * An integer expression is reversible (hence not read-only) if and only if ALL
 * of the following conditions hold:
 *
 * 1. It does not depend on a conditional expression, directly or indirectly
 * 2. After recursively expanding all it's dependencies, it depends on exactly
 *    one free variable
 * 3. After that expansion, the expression is linear with that variable
 */
class IntegerExpressionExpander(precomp: SemanticAnalysis.WidgetAnalysis) extends ASTDeepVisitor {

  /**
   * This function tests whether an integer expression is reversible, and
   * expands it to a linear expression with one free variable in the case where
   * it is expandable. Its return value is determined according to the following
   * rules:
   *
   * - If the expression is not reversible due to being under-constrained and/or
   *   depending on conditionals, the returned value would be (None, reason)
   *   where reason is the reason why this expression can not be expanded to a
   *   linear expression of one free variable (in that case, the expression is
   *   read-only)
   *
   * - If the expression is not reversible due to evaluating to a constant, the
   *   returned value would be (Some(L), ReadOnlyStatus.NothingToUpdate) where
   *   L is the linear expression representing that constant
   *
   * - If the expression is reversible, the returned value would be
   *   (Some(L), ReadOnlyStatus.ReadAndWrite) where L is the linear expression
   *   in one free variable which this attribute evaluates to
   */
  def expand (attr: Attribute): (Option[LinearExpansion], ReadOnlyStatus) = {
    assert(attr.getLeftType == Type.tInt)
    var result = ReadOnlyStatus.ReadAndWrite
    val rv = ResolvedVariable from attr

    if (precomp.freeVariables contains rv) {
      assert (attr.isInstanceOf[InitialAttribute])
      (Some(new LinearExpansion(1,attr.leftSide)), result)
    } else if (attr.isInstanceOf[ExpressionAttribute]) {
      val attrE = attr.asInstanceOf[ExpressionAttribute]

      /* First, test to see if it depends on conditionals */
      if (! ((precomp.dependOnConditionals intersect (precomp.dependencies(rv) + rv)) isEmpty))
        result = result.copy(conditional = true)

      /* Then, test to see how many free variables it depends on */
      var freeCount = 0
      for (prop <- precomp.dependencies(rv))
        if (precomp.freeVariables contains prop)
          freeCount += 1

      if (freeCount > 1)
        result = result.copy(underConstrained = true)

      /* We will handle the case of no free variables in the same way that we
       * handle an expression where the free variables are cancelled during the
       * expansion (like `a-a`) - in both cases we want to calculate the
       * constant result of the expression and we will do this below.
       */

      /* If the result is underConstrained or depends on conditionals, we should
       * return now before trying to expand it */
      if (result != ReadOnlyStatus.ReadAndWrite)
        return (None, result)

      /* Otherwise, let's try to expand the expression! */
      try {
        val expr = expr2linear(attrE.realValue)
        if (expr.isConstant) {
          (Some(expr), ReadOnlyStatus.NothingToUpdate)
        } else {
          (Some(expr), ReadOnlyStatus.ReadAndWrite)
        }
      } catch {
        case nl: NonLinearException =>
          (None, result.copy(nonLinear = true))
      }
    } else {
      /* This is the case where we have an attribute which is not an initial
       * attribute and not an attribute defined by an expression. This shouldn't
       * happen because we defined only these attribute classes!
       */
      throw new AssertionError()
    }
  }


  override def visit(node: Condition): Any = {
    throw new NonLinearException
  }

  override def visit(node: FunctionCall): Any = {
    throw new NonLinearException
  }

  def expr2linear(expr: Expr): LinearExpansion = {
    (expr accept this).asInstanceOf[LinearExpansion]
  }

  override def visit(node: Variable): LinearExpansion = {
    /* If we reached this state, then we are dealing with an integer expression
     * which is not conditional. By the current syntax, integer expressions are
     * made out only of smaller integer expressions, so the variable must be of
     * an integer type
     */
    assert(node.resultType == Type.tInt)
    /* Now that we know this is an integer variable, we can ask for an expansion
     * of it's definition as an integer expression
     */
    if (precomp.freeVariables contains node)
      new LinearExpansion(1, node)
    else
    precomp.integerExpansions.get(ResolvedVariable from node) match {
      /* All the direct dependencies of this variable should have already been
       * analyzed, so we should have a value 
       */
      case None => throw new AssertionError()
      /* Sholdn't happen if we verified the dependencies */
      case Some((None, reason)) => throw new AssertionError()
      /* This should happen */
      case Some((Some(expr), reason)) => expr
    }

  }

  override def visit(node: Sum): LinearExpansion = {
    var result = new LinearExpansion(0)
    for (e <- node.add) {
      result += expr2linear(e)
    }
    for (e <- node.sub) {
      result -= expr2linear(e)
    }
    result
  }

  override def visit(node: Product): LinearExpansion = {
    var result = new LinearExpansion(1)
    for (e <- node.mul) {
      result *= expr2linear(e)
    }
    for (e <- node.div) {
      result /= expr2linear(e)
    }
    result
  }

  override def visit[T](node: Literal[T]): LinearExpansion = {
    assert(node.resultType == Type.tInt)
    new LinearExpansion(node.value.asInstanceOf[Int])
  }
}
